Nuprl Definition : length
11,40
postcript
pdf
||
as
|| == rec-case(
as
) of [] => 0 |
a
::
as'
=>
.||
as'
|| + 1
(recursive)
latex
Definitions
Y
,
x
.
A
(
x
)
,
rec-case(
a
) of [] =>
s
|
x
::
y
=>
z
.
t
(
x
;
y
;
z
)
,
n
+
m
,
f
(
a
)
,
#$n
FDL editor aliases
length
origin
x.A(x)x.A(x)